epistemic situation calculus
Projection in the Epistemic Situation Calculus with Belief Conditionals
Schwering, Christoph (RWTH Aachen University) | Lakemeyer, Gerhard (RWTH Aachen University)
A fundamental task in reasoning about action and change is projection, which refers to determining what holds after a number of actions have occurred. A powerful method for solving the projection problem is regression, which reduces reasoning about the future to reasoning about the initial state. In particular, regression has played an important role in the situation calculus and its epistemic extensions. Recently, a modal variant of the situation calculus was proposed, which allows an agent to revise its beliefs based on so-called belief conditionals as part of its knowledge base. In this paper, we show how regression can be extended to reduce beliefs about the future to initial beliefs in the presence of belief conditionals. Moreover, we show how any remaining belief operators can be eliminated as well, thus reducing the belief projection problem to ordinary first-order entailments.
Decidable Reasoning in a Fragment of the Epistemic Situation Calculus
Lakemeyer, Gerhard (RWTH Aachen University) | Levesque, Hector J. (University of Toronto)
The situation calculus is a popular formalism for reasoning about actions and change. Since the language is first-order, reasoning in the situation calculus is undecidable in general. An important question then is how to weaken reasoning in a principled way to guarantee decidability. Existing approaches either drastically limit the representation of the action theory or neglect important aspects such as sensing. In this paper we propose a model of limited belief for the epistemic situation calculus, which allows very expressive knowledge bases and handles both physical and sensing actions. The model builds on an existing approach to limited belief in the static case. We show that the resulting form of limited reasoning is sound with respect to the original epistemic situation calculus and eventually complete for a large class of formulas. Moreover, reasoning is decidable.